Nuprl Lemma : tree_leaf_wf
4,23
postcript
pdf
E
,
T
:Type,
x
:
E
. tree_leaf(
x
)
tree_con(
E
;
T
)
latex
Definitions
tree_con(
E
;
T
)
,
tree_leaf(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
origin
E, T:Type, x:E. tree_leaf(x) 
tree_con(E;T) E, T:Type, x:E. tree_leaf(x) tree_con(E;T) x:A. B(x) T